import copy
import sys
# 寻找单位子句 返回值1为是否找到 返回值2为单位子句中的文字
def FindUnitP(cnf):
    for item in cnf:
        if len(item)==1:
            return True,item[0]
    return False,-1
# 如果cnf中有两个相冲突的单位子句，则肯定不成立
def NotConflict(cnf,p):
    listp = []
    listp.append(p)
    listNp = []
    listNp.append(-p)
    if listp in cnf and listNp in cnf:
        return False
    return True


def dpll(_cnf,_ans):
    cnf = copy.deepcopy(_cnf)
    ans = _ans.copy()
    #递归出口
    if len(cnf)==0:
        return ans
    # 找到单位子句
    IsReP, p = FindUnitP(cnf)
    #判断是否冲突
    while IsReP:
        if NotConflict(cnf,p):
            ans.append(p)
            cnf = simplify(cnf,p)
        else:
            return []
        IsReP,p = FindUnitP(cnf)
    #再次判断cnf的大小
    if len(cnf)==0:
        return ans
    
    #选取一个长度最小的逻辑子句,并选择其中的第一个变量
    single = cnf[0][0]
    min_clause_size = sys.maxsize
    for items in cnf:
        if min_clause_size > len(items):
            min_clause_size = len(items)
            single = items[0]  
  
    ans.append(single)
    #递归
    x = (dpll(simplify(cnf,single),ans))
    if len(x) !=0:
        return x
    else:
        ans.pop()
        ans.append(-single)
        return dpll(simplify(cnf,-single),ans)

def simplify(_cnf,p):
    cnf = copy.deepcopy(_cnf)
    cnf2 = copy.deepcopy(cnf)
    for item in cnf:
        if p in item:
            cnf2.remove(item)
            continue
    for item in cnf2:
        if -p in item:
            if len(item) == 1:
                return False
            else:
                item.remove(-p)
    return cnf2  #修改前84

def solve(cnf,n):
    dpll_ans = dpll(cnf,[])
    if len(dpll_ans) == 0:
        return None
    else:
        ans = [] 
        for i in range(1,n+1):
            if -i in dpll_ans:
                ans.append(-1)
            else:
                ans.append(1)
        return ans
                
if __name__ == "__main__":
    cnf = [
        [-1, 2],
        [-2, 3],
        [-1, -3],
    ]
    print("ans",solve(cnf,3))